Proving the correctness of a computer program requires knowledge about the program that is not readily available in the program text. For example, loops within a computer program can be proven correct using mathematical induction. However, to do so, one needs to know the loop invariant—a condition that is true when control enters the loop, remains true while the body of the loop is executed, and is still true when control exits the loop. Similarly, to prove the correctness of a class in an object-oriented program, one may need to know what the invariants of the class are, and whether they are preserved. An object invariant is an assertion about a class that is true—most of the time. More specifically, an invariant holds when no method belonging to the object is executing.
Invariants can be difficult to determine. To more specifically consider some of the pitfalls in determining invariants, consider the classes (written in Java-like pseudocode) shown in FIG. 1. For class A 102, the constructor A 104 initializes this.x to “8” 104, and the method M 106 increments this.x subsequently 108. Therefore condition this.x≧8 104 holds on exit from the constructor A 104, on entry to method M 106 and on exit from the method M 109. Thus, we wish to obtain from our analysis that this.x≧8 is an object invariant for A. One way for inferring the object invariant this.x≧8 is to treat the field select expression this.x as denoting one variable, essentially focusing the analysis on one (arbitrary) object at a time. Then, looking at all possible values for this.x the condition this.x≧8 may be inferred, from which can be concluded (∀a:A·a.x≧8).
But this method has problems. Class B 120 illustrates the need to know about properties of objects other than this 124, 128. Focusing only on what can be said about this.x gives no information about another object that might influence this.x, in this case b.x in method B.M 126, which is used to modify the value of this.x 128 in the statement this.x=b.x+1 128. As we currently have no knowledge of the possible values of b.x, 128 we also cannot make any assumptions about the possible values of this.x, and thus we are not be able to establish any information about invariants from our analysis of this piece of code.
Perhaps more critically, class C 132 demonstrates that the existence of aliasing makes the problem even more difficult. In class C 132, the constructor C 134 initializes this.x to “8” 136, as we have seen before. But then Method C.M 138 updates the x field of an object with a name other than this—c.x 140, so it is easy to miss that this update actually occurs on an aliased this object with the result that the analysis would then incorrectly infer this.x=8, which would suggest the fallacious (∀c:C·c.x=8).
A method of inferring object invariants both in the presence of aliasing and when using invariant information about other objects is therefore needed.